a:A fp B(a) == d:(A List)(a:{a:A| (a  d) }B(a)) 

latex

---

clarification:

a:A fp B(a) == d:(A List)(a:{a:A| (a  d  A) }B(a)) 

latex

Definitions	x:AB(x), type List, x:AB(x), {x:A| B(x) }, (x  l)
FDL editor aliases	fpf